Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    min(x,0)  → 0
2:    min(0,y)  → 0
3:    min(s(x),s(y))  → s(min(x,y))
4:    max(x,0)  → x
5:    max(0,y)  → y
6:    max(s(x),s(y))  → s(max(x,y))
7:    x - 0  → x
8:    s(x) - s(y)  → x - y
9:    gcd(s(x),s(y))  → gcd(s(max(x,y)) - s(min(x,y)),s(min(x,y)))
There are 7 dependency pairs:
10:    MIN(s(x),s(y))  → MIN(x,y)
11:    MAX(s(x),s(y))  → MAX(x,y)
12:    s(x) -# s(y)  → x -# y
13:    GCD(s(x),s(y))  → GCD(s(max(x,y)) - s(min(x,y)),s(min(x,y)))
14:    GCD(s(x),s(y))  → s(max(x,y)) -# s(min(x,y))
15:    GCD(s(x),s(y))  → MAX(x,y)
16:    GCD(s(x),s(y))  → MIN(x,y)
The approximated dependency graph contains 4 SCCs: {12}, {11}, {10} and {13}.
Tyrolean Termination Tool  (0.17 seconds)   ---  May 4, 2006